(set-logic BV)
(synth-fun f ( (x (BitVec 64)) ) (BitVec 64)
((Start (BitVec 64)
((bvnot Start)
(bvxor Start Start)
(bvand Start Start)
(bvor Start Start)
(bvneg Start)
(bvadd Start Start)
(bvmul Start Start)
(bvudiv Start Start)
(bvurem Start Start)
(bvlshr Start Start)
(bvashr Start Start)
(bvshl Start Start)
(bvsdiv Start Start)
(bvsrem Start Start)
(bvsub Start Start)
x
#x0000000000000000
#x0000000000000001
#x0000000000000002
#x0000000000000003
#x0000000000000004
#x0000000000000005
#x0000000000000006
#x0000000000000007
#x0000000000000008
#x0000000000000009
#x0000000000000009
#x0000000000000009
#x000000000000000A
#x000000000000000B
#x000000000000000C
#x000000000000000D
#x000000000000000E
#x000000000000000F
#x0000000000000010
(ite StartBool Start Start)
))
(StartBool Bool
((= Start Start)
(not StartBool)
(and StartBool StartBool)
(or StartBool StartBool)
))))
(constraint (= (f #x4a62d5e781c3dee8) #x25316af3c0e1ef74))
(constraint (= (f #x845ee1528170cdab) #x422f70a940b866d5))
(constraint (= (f #x794867c3070d4782) #x3ca433e18386a3c1))
(constraint (= (f #x80edee2729694555) #x4076f71394b4a2aa))
(constraint (= (f #x2a266c8d3eae9780) #x151336469f574bc0))
(constraint (= (f #x71d64323725ed881) #x38eb2191b92f6c40))
(constraint (= (f #x953e8c1e588ebb8e) #x4a9f460f2c475dc7))
(constraint (= (f #x0207146462be3442) #x01038a32315f1a21))
(constraint (= (f #x0e6b064851280644) #x0735832428940322))
(constraint (= (f #xed4bee115eb1c195) #x76a5f708af58e0ca))
(constraint (= (f #x4420e121260b563a) #x221070909305ab1d))
(constraint (= (f #x9bea4eeb62e6ca27) #x4df52775b1736513))
(constraint (= (f #x7e70e67538017862) #x3f38733a9c00bc31))
(constraint (= (f #xee8aad867a898b2e) #x774556c33d44c597))
(constraint (= (f #x0ab5b4eda6d425cc) #x055ada76d36a12e6))
(constraint (= (f #x15857eb02a38e0b4) #x0ac2bf58151c705a))
(constraint (= (f #x90d9bdbe4014e994) #x486cdedf200a74ca))
(constraint (= (f #xe7ac87ec7364ee74) #x73d643f639b2773a))
(constraint (= (f #x9244dee818e3a95d) #x49226f740c71d4ae))
(constraint (= (f #xce85a30decce9e05) #x6742d186f6674f02))
(constraint (= (f #x0dd81e49a3de92dd) #x06ec0f24d1ef496e))
(constraint (= (f #xe185e467c977e780) #x70c2f233e4bbf3c0))
(constraint (= (f #x8578cc8d30c65628) #x42bc664698632b14))
(constraint (= (f #x729ee678678ea8dd) #x394f733c33c7546e))
(constraint (= (f #x16252ee16e82c92a) #x0b129770b7416495))
(constraint (= (f #x6c079ebe56c3e501) #x3603cf5f2b61f280))
(constraint (= (f #xb577a42140e7be4b) #x5abbd210a073df25))
(constraint (= (f #xd0491e340a83a31b) #x68248f1a0541d18d))
(constraint (= (f #x54638933254e5b79) #x2a31c49992a72dbc))
(constraint (= (f #xb095b96b032ac503) #x584adcb581956281))
(constraint (= (f #xa22b8244ea1433d6) #x5115c122750a19eb))
(constraint (= (f #x573992a1cc06c184) #x2b9cc950e60360c2))
(constraint (= (f #xee762288424d3364) #x773b1144212699b2))
(constraint (= (f #x34ee637634eeec2e) #x1a7731bb1a777617))
(constraint (= (f #x1aeaedabb93b45a4) #x0d7576d5dc9da2d2))
(constraint (= (f #xea9392aa5025e6a7) #x7549c9552812f353))
(constraint (= (f #x6b77d205db23edee) #x35bbe902ed91f6f7))
(constraint (= (f #x7389da07d1335887) #x39c4ed03e899ac43))
(constraint (= (f #xae7d77476b7b1bcd) #x573ebba3b5bd8de6))
(constraint (= (f #x78ded6e9d7bacc63) #x3c6f6b74ebdd6631))
(constraint (= (f #xe4b8e29856a62e52) #x725c714c2b531729))
(constraint (= (f #x5ebad130ee2e3206) #x2f5d689877171903))
(constraint (= (f #x2bbe4ce7be3ecad6) #x15df2673df1f656b))
(constraint (= (f #xbe00525d7abcd985) #x5f00292ebd5e6cc2))
(constraint (= (f #x7c50da8debbc64d2) #x3e286d46f5de3269))
(constraint (= (f #xce8aa8590e2689bd) #x6745542c871344de))
(constraint (= (f #x96d15de0269955c8) #x4b68aef0134caae4))
(constraint (= (f #x309b2dd6e0c3e734) #x184d96eb7061f39a))
(constraint (= (f #x5269d15ec9a9119e) #x2934e8af64d488cf))
(constraint (= (f #xec24ceec8dae9486) #x7612677646d74a43))
(constraint (= (f #xc3ab55a006bc3898) #x61d5aad0035e1c4c))
(constraint (= (f #x54362e2b37b6d17e) #x2a1b17159bdb68bf))
(constraint (= (f #xb1059cbda9053c77) #x5882ce5ed4829e3b))
(constraint (= (f #xd2d03d4ad29d283d) #x69681ea5694e941e))
(constraint (= (f #x3c80ce4d2245e2d8) #x1e4067269122f16c))
(constraint (= (f #xc1bde9ac20a0e56e) #x60def4d6105072b7))
(constraint (= (f #xa4a14e59494465d3) #x5250a72ca4a232e9))
(constraint (= (f #x859e3e1215ee709e) #x42cf1f090af7384f))
(constraint (= (f #x6bdca0965e08293e) #x35ee504b2f04149f))
(constraint (= (f #x5407d148903b4c43) #x2a03e8a4481da621))
(constraint (= (f #x71252d876c4cae17) #x389296c3b626570b))
(constraint (= (f #x51890aa66e0626eb) #x28c4855337031375))
(constraint (= (f #x4a46e6cdae40c872) #x25237366d7206439))
(constraint (= (f #x7ce1036ce833533c) #x3e7081b67419a99e))
(constraint (= (f #x4ea62eb559105d42) #x2753175aac882ea1))
(constraint (= (f #x902364e80ec7cd5e) #x4811b2740763e6af))
(constraint (= (f #x1121662d76055175) #x0890b316bb02a8ba))
(constraint (= (f #x571d4c0a20268c91) #x2b8ea60510134648))
(constraint (= (f #x1ce1200b4e3e8d6c) #x0e709005a71f46b6))
(constraint (= (f #x0d4b592078d67549) #x06a5ac903c6b3aa4))
(constraint (= (f #x9c069cea5be91027) #x4e034e752df48813))
(constraint (= (f #xed0586bae6dee00e) #x7682c35d736f7007))
(constraint (= (f #x294ab215e90b04b0) #x14a5590af4858258))
(constraint (= (f #xd7319ea0de2c2a2c) #x6b98cf506f161516))
(constraint (= (f #x108ab83b466385c7) #x08455c1da331c2e3))
(constraint (= (f #xeca3075660e43c56) #x765183ab30721e2b))
(constraint (= (f #x138b3de579e28e4e) #x09c59ef2bcf14727))
(constraint (= (f #x79c3e92567d4c667) #x3ce1f492b3ea6333))
(constraint (= (f #xe596509a2d2cbacd) #x72cb284d16965d66))
(constraint (= (f #xc4e4819690566988) #x627240cb482b34c4))
(constraint (= (f #x2eeb7c15e951ebce) #x1775be0af4a8f5e7))
(constraint (= (f #xd7cbed1eace6e07a) #x6be5f68f5673703d))
(constraint (= (f #x060eeed0c341aebc) #x0307776861a0d75e))
(constraint (= (f #x59b25a166d016cdd) #x2cd92d0b3680b66e))
(constraint (= (f #xbb377ce21e054da3) #x5d9bbe710f02a6d1))
(constraint (= (f #xb9bc93d8e07c74c3) #x5cde49ec703e3a61))
(constraint (= (f #x256d6a04d2ee36ca) #x12b6b50269771b65))
(constraint (= (f #x936413d2e8c4ca34) #x49b209e97462651a))
(constraint (= (f #x19792b847ec21e89) #x0cbc95c23f610f44))
(constraint (= (f #x7e8c4378ed9e13b8) #x3f4621bc76cf09dc))
(constraint (= (f #x27a7172c98ba7ecd) #x13d38b964c5d3f66))
(constraint (= (f #xba97246b404773b4) #x5d4b9235a023b9da))
(constraint (= (f #x83568e3a1beda244) #x41ab471d0df6d122))
(constraint (= (f #x61327e097ca79362) #x30993f04be53c9b1))
(constraint (= (f #x67ee04586e847c4c) #x33f7022c37423e26))
(constraint (= (f #xe7b6ed123e2a4424) #x73db76891f152212))
(constraint (= (f #xa3417e1ea8dbdd25) #x51a0bf0f546dee92))
(constraint (= (f #x8e1144b950d42a63) #x4708a25ca86a1531))
(constraint (= (f #xe17ceb9ee4162040) #x70be75cf720b1020))
(constraint (= (f #x9155e9e0d264424a) #x48aaf4f069322125))
(check-synth)
(define-fun f_1 ((x (BitVec 64))) (BitVec 64) (bvudiv x #x0000000000000002))
